A:MsgA. A ||  

latex

Definitions	, M1 || M2, M1 ||decl M2, MsgA, mk-ma, Valtype(da;k), P & Q, IdDeq, KindDeq, locl(a), Prop, IdLnkDeq, State(ds), 1of(t), f(x)?z, rcv(l,tg), 2of(t), Top, product-deq(A;B;a;b), a:A fp B(a), x. t(x), x:A. B(x), Id, IdLnk, t  T, Knd
Lemmas	fpf-trivial-subtype-top, product-deq wf, pi2 wf, rcv wf, fpf-cap wf, top wf, pi1 wf, ma-state wf, idlnk-deq wf, IdLnk wf, locl wf, Knd wf, Kind-deq wf, Id wf, id-deq wf, fpf-empty-compatible-right, msga wf